Storm-static

Benchmark
Model:nand v.1 (DTMC)
Parameter(s)N = 60, K = 4
Property:reliable (prob-reach)
Invocation (default)
~/storm/build/bin/storm --prism nand.prism --prop nand.props reliable --constants N=60,K=4 --exact floats --general:precision 1e-20  --ddlib sylvan --sylvan:maxmem 6114 --sylvan:threads 4
Execution
Walltime:89.49804878234863s
Return code:0
Note(s):The tool result '686721458919267724319013/1000000000000000000000000' is tagged as incorrect. The reference result is '674375412048286579998391053568044024839796891188436079164933195932504006859863176668618453626567200815744325954013096026732016576292941767289283443813273798927471369808814227780678597502526283170376011143732046040738638479975488052191318262796730887423499092060055764460808570555973414684635167757065338750791739331293858988603042989487945582955712491974590260039905065741873854885714298872588020623965467400282885463166739143535812717697199273310102277971278786945528949661789220074183715013841242260836804042248270660085557976363578175644872898551287821380993759020250450057165990145439180550980345336796910958837967490732422873158833390335926967641639016077401593504779192627736207826140866888177394711176343476439862638983111578860864406915339169201668448685867985486117826497430887145901618112836384648567977530826248389205029495657410593836586948449805252838334427173444580925770987996143922689432502457408017259242081442839253964797127083172809304607437564123586401108004199299044292446541/982021754656721722716655706411222385507669639910781715967345406263201783692889897878427213212990938612763788231403389744767067663614743521859183275654310118412922964549494284527781431535499684177432434122301448144083942764451247133599577036672904647064298810598161393171352158933989819282448394583468262131119361851408297476380158691952302398288740119725979550137284712658047394731931729250052156222114008241553695693345821266964444821100463081039235040824849892155915658833109729829406529861748248993399079598686019016345103724868380607355278949134904844556514833763239300674164534870820578969104145515316399053092033353590698921512459580587666964268557149107720604442375672662685956383159528500472087293439870951895677831469622118461029958936824764580705546202761417280408696752629675501504845173358369477857440457221826064912064573000278911442195364772677516118775811496516055643960074429058958872529316863619897048920392990112304687500000000000000000000000000000000000000000000000000000000000' (approx. 0.6867214589192305) which means a relative error of '5.4205061836599116e-14' which is larger than the goal precision '1e-14'.
Relative Error:5.4205061836599116e-14
Log
Storm 1.5.1

Date: Tue Apr 28 13:09:03 2020
Command line arguments: --prism nand.prism --prop nand.props reliable --constants 'N=60,K=4' --exact floats '--general:precision' 1e-20 --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4
Current working directory: /

 WARN (GeneralSettings.cpp:110): Setting the precision option with module prefix does not effect all solvers. Consider setting --precision instead of --general:precision.
Time for model input parsing: 0.021s.

Time for model construction: 70.766s.

-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	18826082
Transitions: 	29772212
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * ((s = 4) & ((z / 60) < 1/10)) -> 6 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "reliable": P=? [F ((s = 4) & ((z / 60) < 1/10))] ...
Result (for initial states): 0.686721458919267724319013
Time for model checking: 18.431s.